Inference at * 1 
Iof proof for Lemma member-zip:



1. A : Type
2. B : Type
3. A List
  ys:(B List), x:A, y:B. (<x, y>  zip([];ys))  {(x  []) & (y  ys)} 

latex

 by Reduce 0 THEN Auto THEN ObviousFrom [(-1)] 

latex

 .

Definitions	P  Q, False, x:AB(x), P  Q, x:A. B(x), [], t  T, {T}, P & Q, , {x:A| B(x)} , , A  B, A, a < b, ||as||, Y, x.A(x), rec-case(a) of [] => s | x::y => z.t(x;y;z), n+m, s = t, l[i], hd(l), nth_tl(n;as), if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), i z j, b, i <z j, if a<b then c else d, n - m, tl(l), Type, type List, x:A  B(x), <a, b>, (x  l)
Lemmas	nil member, l member wf